es:ES, a:Atom1, e:E.
((state when e):state@loc(e)>>a
( first(e)
( loc(e) >> a
(  (state when pred(e)):state@loc(pred(e))>>a
(  isrcv(pred(e)) & val(pred(e)):valtype(pred(e))>>a)
& (e sends a
& ( loc(e) >> a  (state when e):state@loc(e)>>a  isrcv(e) & val(e):valtype(e)>>a) 

latex

Definitions

t  T, x:A. B(x), P  Q, Void, f(a), type List, Unit, locl(a), left+right, Id, state@i, S  T, vartype(i;x), S  T, P  Q, x:T>>a, Msg, s = t, Prop, {T}, i >> a, x:AB(x), val(e), valtype(e), isrcv(e), b, A & B, (state when e), pred(e), A/x,y. B(x;y), 1of(t), E, first(e), A, e sends a, P & Q, (x  l), Atom$n, ES, loc(e), kindtype(i;k), x.A(x), Type, Knd, x:AB(x), AtomFree(T;x), Choose(i), Send(i), Trans(i)

Lemmas

event system wf, es-machine-axiom, es-E wf, implies-es-atom-axiom, es-send-atom wf, not wf, es-first wf, es-pred wf, es-state-when wf, assert wf, es-isrcv wf, es-valtype wf, es-val wf, es-atom wf, atom-free-es-valtype, es-choose wf, es-send wf, es-Msg wf, inheres wf, es-trans wf, es-vartype wf, es-state wf, atom-free-es-Msg, atom-free-es-state, Id wf, locl wf, unit wf, Knd wf, es-kindtype wf, atom-free-es-kindtype, es-loc wf, atom-free-Knd